es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p,
q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
e1  e2   q(e1,e2)  [e1;e2]~([a,b].p(a,b))*[a,b].q(a,b) 

latex

Definitions	{i..j}, E, Id, e  e' , P & Q, (e <loc e'), x:A. B(x), x(s1,s2), x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), ES, t  T, loc(e), Prop, P  Q, , False, A, AB, i  j < k, b, pred(e), 1of(t), P  Q, A & B, x. t(x), P  Q, P  Q
Lemmas	or functionality wrt iff, int seg properties, nat plus properties, all functionality wrt iff, es-locl-iff, es-locl wf, es-pred wf, es-le-loc, es-loc-pred, le wf, subtype rel self, int seg wf, es-le wf, Id wf, es-loc wf, es-E wf, event system wf